M1, M2:MsgA. M1  M2  (k:Knd, x:Id. M2.aframe(k affects x)  M1.aframe(k affects x)) 

latex

Definitions	x:AB(x), A & B, t  T, P  Q, x:A. B(x), f  g, Id, x:AB(x), True, Knd, type List, f(x), <a,b>, s = t, IdDeq, T, Type, EqDecider(T), deq-member(eq;x;L), Prop, , b, IdLnk, x.A(x), x. t(x), Top, a:A fp B(a), KindDeq, x  dom(f), z != f(x)  P(a;z), P & Q, Valtype(da;k), MsgA, M1  M2, M.aframe(k affects x)
Lemmas	ma-aframe wf, ma-sub wf, msga wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, Knd wf, assert wf, bool wf, deq-member wf, squash wf, true wf, deq wf, Id wf, id-deq wf